Termination Proof Script
Consider the TRS R consisting of the rewrite rules
1:
app
(
app
(
.
,
1
),x)
→ x
2:
app
(
app
(
.
,x),
1
)
→ x
3:
app
(
app
(
.
,
app
(
i
,x)),x)
→
1
4:
app
(
app
(
.
,x),
app
(
i
,x))
→
1
5:
app
(
app
(
.
,
app
(
i
,y)),
app
(
app
(
.
,y),z))
→ z
6:
app
(
app
(
.
,y),
app
(
app
(
.
,
app
(
i
,y)),z))
→ z
7:
app
(
i
,
1
)
→
1
8:
app
(
i
,
app
(
i
,x))
→ x
There are no dependency pairs. Hence the TRS is trivially terminating.
Tyrolean Termination Tool
(0.01 seconds) --- May 4, 2006